Nuprl Lemma : w-after-lemma2 0,22

w:World. FairFifo  (e:E, x:Id. state_after(e).x = (x after e vartype(loc(e);x)) 
latex


Definitionst  T, x:AB(x), P  Q, World, FairFifo, E, Id, state_after(e), s.x, <a,b>, s = t, loc(e), vartype(i;x)
LemmasId wf, w-E wf, fair-fifo wf, world wf, w-after-lemma, subtype rel self, w-vartype wf, w-loc wf

origin